Train Cross Control Example

Train Cross Control Example

In this example, we model a railway control system to automatically control trains passing a critical point such as a bridge. The idea is to use a computer to guide trains from several tracks crossing a single bridge instead of building many bridges. Obviously, a safety-property of such a system is to avoid the situation where more than one train are crossing the bridge at the same time.

For more details about this example, see "Automatic Verification of Real-Time Communicating Systems by Constraint Solving", by Wang Yi, Paul Pettersson and Mats Daniels. In Proceedings of the 7th International Conference on Formal Description Techniques, pages 223-238, North-Holland. 1994.

#import "PAT.Lib.Queue";
//number of trains
#define N 4;
channel appr 0;
channel go 0;
channel leave 0;
channel stop 0;
var<Queue> queue;
//Train model with 'within'
Train(i) = appr!i -> ((Wait[10, 20]; Cross(i)) [ ] (stop?i -> StopS(i) within[10]));
Cross(i) = (leave!i -> Train(i)) within[3,5];
StopS(i) = go?i -> Start(i);
Start(i) = Wait[7, 15] ; Cross(i);
Gate = if (queue.Count() ==0) {
atomic{appr?i -> tau{queue.Enqueue(i)} -> Skip}; Occ
} else {

within

};
Occ = (atomic{leave?[i == queue.First()]i -> tau{queue.Dequeue()} -> Skip}; Gate)
[ ]
(atomic{appr?i -> tau{queue.Enqueue(i)} -> stop!queue.Last() -> Skip}; Occ);
System = ( | | | x:{0..N-1} @Train(x)) | | | Gate;
#assert System deadlockfree;
//Whenever a train approaches the bridge, it will eventually cross.
#assert System |= [] (appr!1 -> <>leave!1);
//overflow: There can never be N elements in the queue (thus the array will not overflow).
#define overflow (queue.Count()> N);
#assert System reaches overflow;